ePMC

Benchmark

Model:	beb v.1 (MDP)
Parameter(s)	H = 5, K = 16, N = 15
Property:	LineSeized (prob-reach)

Invocation (default)

java -Xms10240m -Xmx10240m -jar ./root/epmc-standard.jar check --model-input-files beb.5-16.jani --model-input-type jani --property-input-names LineSeized --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const N=15

Execution

Walltime:	2.48786997795105s
Return code:	0
Note(s):	Correctness of result is not checked because no reference result is available.

Log

assertions-disabled
model-checking
analysing-property LineSeized
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-done 1 0
iterating
iterating-done 1 0
num-states-in-filter 1 "initial"
model-checking-done 1
command-check-result-is 0.0 LineSeized